$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$), $e$:E($X$). $X$($e$) $\in$ $A$